T:(IdType), tab:secret-table(T).
atoms-distinct(tab)
 (x:Atom1, n:||tab|| .
 (nptr(tab)
 ( st-atom(tab;n) = x
 ( isl(st-lookup(tab;x))
 ( & outl(st-lookup(tab;x)) = <key(tab;n),data(tab;n)>  (+Atom1)data(T)) 

latex

Definitions	A & B, Type, t  T, Id, x:AB(x), x:A. B(x), secret-table(T), atoms-distinct(tab), Atom$n, , {x:A| B(x) }, ||tab|| , #$n, {i..j}, ptr(tab), AB, st-atom(tab;n), s = t, Prop, P  Q, x:AB(x), P & Q, x:A. B(x), a<b, Void, False, A, i  j < k, , P  Q, P  Q, <a,b>, {T}, SQType(T), s ~ t, data(tab;n), key(tab;n), left+right, data(T), Unit, st-lookup(tab;x), outl(x)
Lemmas	st-lookup-outl, st-lookup-property, st-atom wf, le wf, st-ptr wf, int seg wf, st-length wf, nat wf, st-atoms-distinct wf, secret-table wf, Id wf